$\forall$$M_{1}$, $M_{2}$:msga\{i:l\}. ma{-}compatible{-}decls\{i:l\}($M_{1}$; $M_{2}$) $\in$ Prop$_{\mbox{\scriptsize i'}}$